VERS5 
NIL 
((IRREFLEXIVITY_OF_ORDER NATNUM#7) (TRANSITIVITY_OF_ORDER NATNUM#8) (ZEROLEAST1 NATNUM#9) (SUCCESSOR1 NATNUM#11) (SUCCESSOR2 NATNUM#12) (SUCCESSORLESS NATNUM#13) (SUCCESSOREQ NATNUM#14) (ZEROLEAST2 NATNUM#15) (ZEROLEAST3 NATNUM#16) (ZERO_NOT_SUCCESSOR NATNUM#17) (PLUSDEF1 NATNUM#24) (LPLUSCAN NATNUM#26) (RPLUSCAN NATNUM#27) (ADDTOZERO NATNUM#28) (COMMUTADD NATNUM#29) (TIMESDEF NATNUM#30) (TIMSUCC NATNUM#33) (LTIMESCAN NATNUM#34) (RTIMESCAN NATNUM#35) (COMMUTMULT NATNUM#36) (LTIMESTOZERO NATNUM#37) (RTIMESTOZERO NATNUM#38) (LDISTRIB NATNUM#39) (RDISTRIB NATNUM#40) (PROOF_BY_INDUCTION INDUCTION#1) (INDUCTIVE_DEFINITION INDUCTION#5) (PROOF_BY_DOUBLEINDUCTION INDUCTION#6) (HIGH_ORDER_NATNUM_DEFINITION INDUCTION#10) (INFINITE_DESCENT INDUCTION#11) (SUCCFACTS NATNUM#11 NATNUM#12 NATNUM#13 NATNUM#14 NATNUM#15 NATNUM#16 NATNUM#17) (TIMESFACTS NATNUM#30 NATNUM#32 NATNUM#33 NATNUM#34 NATNUM#35 NATNUM#36 NATNUM#37 NATNUM#38 NATNUM#39 NATNUM#40) (PLUSFACTS NATNUM#21 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 NATNUM#29 NATNUM#39 NATNUM#40) (SIMPINFO NATNUM#10 NATNUM#19 NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23 NATNUM#24 NATNUM#25 NATNUM#30 NATNUM#31 NATNUM#32)) (NIL . (DECL LESSP (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|)) (SYNTYPE: CONSTANT) (INFIXNAME: <) (BINDINGPOWER: 920)) . ((LESSP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . <)) . NATNUM#1 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 1 .)(NIL . (DECL ADD1 (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT) (POSTFIXNAME: /') (BINDINGPOWER: 975)) . ((ADD1 . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 975) (POSTFIX& . /')) . NATNUM#2 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 2 .)(NIL . (DECL PLUS (INFIXNAME: +) (TYPE: (TY& . |(GROUND⊗GROUND⊗(GROUND*))→GROUND|)) (SYNTYPE: CONSTANT) (ASSOCIATIVITY: BOTH) (BINDINGPOWER: 930)) . ((PLUS . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 930) (INFIX& . +)) . NATNUM#3 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 3 .)(NIL . (DECL TIMES (TYPE: (TY& . |(GROUND⊗GROUND⊗(GROUND*))→GROUND|)) (SYNTYPE: CONSTANT) (INFIXNAME: *) (ASSOCIATIVITY: BOTH) (BINDINGPOWER: 935)) . ((TIMES . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 935) (INFIX& . *)) . NATNUM#4 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 4 .)(NIL . (DECL (I J K N M) (SORT: (TM& . NATNUM)) (TYPE: (TY& . GROUND))) . ((M . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#5 . NIL . VARIABLE .)) (N . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#5 . NIL . VARIABLE .)) (K . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#5 . NIL . VARIABLE .)) (J . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#5 . NIL . VARIABLE .)) (I . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#5 . NIL . VARIABLE .))) . NIL . NIL . NIL . NATNUM . NIL . 5 .)(NIL . (DECL (A B C SET) (TYPE: (TY& . GROUND→TRUTHVAL))) . ((SET . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#6 . NIL . VARIABLE .)) (C . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#6 . NIL . VARIABLE .)) (B . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#6 . NIL . VARIABLE .)) (A . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#6 . NIL . VARIABLE .))) . NIL . NIL . NIL . NATNUM . NIL . 6 .)(|∀N.¬N<N| . (AXIOM (TM& . |∀N.¬N<N|)) . (LESSP M N K J I) . NIL . (NATNUM#7) . NIL . NATNUM . NIL . 7 .)(|∀N M K.N<M∧M<K⊃N<K| . (AXIOM (TM& . |∀N M K.N<M∧M<K⊃N<K|)) . (LESSP M N K J I) . NIL . (NATNUM#8) . NIL . NATNUM . NIL . 8 .)(|∀N.¬N<0| . (AXIOM (TM& . |∀N.¬N<0|)) . (LESSP M N K J I) . NIL . (NATNUM#9) . NIL . NATNUM . NIL . 9 .)(|∀N.NATNUM(N')| . (AXIOM (TM& . |∀N.NATNUM(N')|)) . (ADD1 M N K J I) . NIL . (NATNUM#10) . NIL . NATNUM . NIL . 10 .)(|∀N.N<N'| . (AXIOM (TM& . |∀N.N<N'|)) . (LESSP ADD1 M N K J I) . NIL . (NATNUM#11) . NIL . NATNUM . NIL . 11 .)(|∀N M.¬N<M⊃M<N'| . (AXIOM (TM& . |∀N M.¬N<M⊃M<N'|)) . (LESSP ADD1 M N K J I) . NIL . (NATNUM#12) . NIL . NATNUM . NIL . 12 .)(|∀N M.N'<M'≡N<M| . (AXIOM (TM& . |∀N M.N'<M'≡N<M|)) . (LESSP ADD1 M N K J I) . NIL . (NATNUM#13) . NIL . NATNUM . NIL . 13 .)(|∀N M.N'=M'≡N=M| . (AXIOM (TM& . |∀N M.N'=M'≡N=M|)) . (ADD1 M N K J I) . NIL . (NATNUM#14) . NIL . NATNUM . NIL . 14 .)(|∀N.¬N=0⊃0<N| . (AXIOM (TM& . |∀N.¬N=0⊃0<N|)) . (LESSP M N K J I) . NIL . (NATNUM#15) . NIL . NATNUM . NIL . 15 .)(|∀N.0<N'| . (AXIOM (TM& . |∀N.0<N'|)) . (LESSP ADD1 M N K J I) . NIL . (NATNUM#16) . NIL . NATNUM . NIL . 16 .)(|∀N.¬N'=0| . (AXIOM (TM& . |∀N.¬N'=0|)) . (ADD1 M N K J I) . NIL . (NATNUM#17) . NIL . NATNUM . NIL . 17 .)(NIL . (DECL PRED (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT)) . ((PRED . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#18 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 18 .)(|∀N.PRED(N')=N| . (DEFAX PRED (TM& . |∀N.PRED(N')=N|)) . (ADD1 M N K J I (PRED . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#19 . NIL . DEFINED .))) . NIL . (NATNUM#19) . NIL . NATNUM . NIL . 19 .)(|∀A.A(0)∧(∀N.A(N)⊃A(N'))⊃(∀N.A(N))| . (AXIOM (TM& . |∀A.A(0)∧(∀N.A(N)⊃A(N'))⊃(∀N.A(N))|)) . (ADD1 M N K J I SET C B A) . NIL . (INDUCTION#1) . NIL . INDUCTION . NIL . 1 .)(NIL . (DECL NPARS (TYPE: (TY& . GROUND*))) . ((NPARS . (GROUND* . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#2 . NIL . VARIABLE .))) . NIL . NIL . NIL . INDUCTION . NIL . 2 .)(NIL . (DECL NDF (TYPE: (TY& . |(GROUND⊗(GROUND*))→(GROUND*)|))) . ((NDF . (|(GROUND⊗(GROUND*))→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#3 . NIL . VARIABLE .))) . NIL . NIL . NIL . INDUCTION . NIL . 3 .)(NIL . (DECL ZCASE (TYPE: (TY& . |(GROUND*)→GROUND|))) . ((ZCASE . (|(GROUND*)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#4 . NIL . VARIABLE .))) . NIL . NIL . NIL . INDUCTION . NIL . 4 .)(|∀N.NATNUM(PRED(N))| . (AXIOM (TM& . |∀N.NATNUM(PRED(N))|)) . (ADD1 M N K J I PRED) . NIL . (NATNUM#20) . NIL . NATNUM . NIL . 20 .)(|∀N K.0+N=N∧K'+N=(K+N)'| . (DEFAX PLUS (TM& . |∀N K.0+N=N∧K'+N=(K+N)'|)) . (ADD1 (PLUS . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 930) (INFIX& . +)) . NATNUM#21 . NIL . DEFINED .)) M N K J I) . NIL . (NATNUM#21) . NIL . NATNUM . NIL . 21 .)(|∀NDF ZCASE NDEF.(∃FUN.(∀NPARS N.FUN(0,NPARS)=ZCASE(NPARS)∧ FUN(N',NPARS)= NDEF(N,FUN(N,NDF(N,NPARS)),NPARS)))| . (AXIOM (TM& . |∀NDF ZCASE NDEF.(∃FUN.(∀NPARS N.FUN(0,NPARS)=ZCASE(NPARS)∧ FUN(N',NPARS)= NDEF(N,FUN(N,NDF(N,NPARS)),NPARS)))|)) . (ADD1 M N K J I NPARS NDF ZCASE (FUN . (|(GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#5 . NIL . VARIABLE .)) (NDEF . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#5 . NIL . VARIABLE .))) . NIL . (INDUCTION#5) . NIL . INDUCTION . NIL . 5 .)(|∀A2.(∀N M.A2(0,N)∧A2(N,0)∧(A2(N,M)⊃A2(N',M')))⊃(∀N M.A2(N,M))| . (AXIOM (TM& . |∀A2.(∀N M.A2(0,N)∧A2(N,0)∧(A2(N,M)⊃A2(N',M')))⊃(∀N M.A2(N,M))|)) . (ADD1 M N K J I (A2 . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#6 . NIL . VARIABLE .))) . NIL . (INDUCTION#6) . NIL . INDUCTION . NIL . 6 .)(NIL . (DECL (ARB ARB1 ARB2) (TYPE: (TY& . ?ARBITRARY))) . ((ARB2 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#7 . NIL . VARIABLE .)) (ARB1 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#7 . NIL . VARIABLE .)) (ARB . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#7 . NIL . VARIABLE .))) . NIL . NIL . NIL . INDUCTION . NIL . 7 .)(|∀N M.NATNUM(N+M)| . (AXIOM (TM& . |∀N M.NATNUM(N+M)|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#22) . NIL . NATNUM . NIL . 22 .)(|∀N.N+0=N| . (AXIOM (TM& . |∀N.N+0=N|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#23) . NIL . NATNUM . NIL . 23 .)(|∀N.1+N=N'∧N+1=N'| . (AXIOM (TM& . |∀N.1+N=N'∧N+1=N'|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#24) . NIL . NATNUM . NIL . 24 .)(|∀N K.N+K'=(N+K)'| . (AXIOM (TM& . |∀N K.N+K'=(N+K)'|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#25) . NIL . NATNUM . NIL . 25 .)(|∀N K M.K+M=K+N≡M=N| . (AXIOM (TM& . |∀N K M.K+M=K+N≡M=N|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#26) . NIL . NATNUM . NIL . 26 .)(|∀N K M.M+K=N+K≡M=N| . (AXIOM (TM& . |∀N K M.M+K=N+K≡M=N|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#27) . NIL . NATNUM . NIL . 27 .)(|∀N K.N+K=0≡N=0∧K=0| . (AXIOM (TM& . |∀N K.N+K=0≡N=0∧K=0|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#28) . NIL . NATNUM . NIL . 28 .)(|∀K N.K+N=N+K| . (AXIOM (TM& . |∀K N.K+N=N+K|)) . (ADD1 PLUS M N K J I) . NIL . (NATNUM#29) . NIL . NATNUM . NIL . 29 .)(|∀N K.0*N=0∧N'*K=N*K+K| . (DEFAX TIMES (TM& . |∀N K.0*N=0∧N'*K=N*K+K|)) . (ADD1 PLUS (TIMES . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 935) (INFIX& . *)) . NATNUM#30 . NIL . DEFINED .)) M N K J I) . NIL . (NATNUM#30) . NIL . NATNUM . NIL . 30 .)(NIL . (DECL INDFN (TYPE: (TY& . |(GROUND⊗(@ARB))→(@ARB)|))) . ((INDFN . (|(GROUND⊗(@ARB))→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#8 . NIL . VARIABLE .)) ARB) . NIL . NIL . NIL . INDUCTION . NIL . 8 .)(NIL . (DECL (DEF_FUN) (TYPE: (TY& . |GROUND→(@ARB)|))) . ((DEF_FUN . (|GROUND→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#9 . NIL . VARIABLE .)) ARB) . NIL . NIL . NIL . INDUCTION . NIL . 9 .)(|∀N M.NATNUM(M*N)| . (AXIOM (TM& . |∀N M.NATNUM(M*N)|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#31) . NIL . NATNUM . NIL . 31 .)(|∀N.N*0=0∧1*N=N∧N*1=N| . (AXIOM (TM& . |∀N.N*0=0∧1*N=N∧N*1=N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#32) . NIL . NATNUM . NIL . 32 .)(|∀N K.N*K'=N*K+N| . (AXIOM (TM& . |∀N K.N*K'=N*K+N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#33) . NIL . NATNUM . NIL . 33 .)(|∀N K M.¬K=0⊃K*M=K*N≡M=N| . (AXIOM (TM& . |∀N K M.¬K=0⊃K*M=K*N≡M=N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#34) . NIL . NATNUM . NIL . 34 .)(|∀N K M.¬K=0⊃M*K=N*K≡M=N| . (AXIOM (TM& . |∀N K M.¬K=0⊃M*K=N*K≡M=N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#35) . NIL . NATNUM . NIL . 35 .)(|∀N M.N*M=M*N| . (AXIOM (TM& . |∀N M.N*M=M*N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#36) . NIL . NATNUM . NIL . 36 .)(|∀N K.¬N=0⊃N*K=0≡K=0| . (AXIOM (TM& . |∀N K.¬N=0⊃N*K=0≡K=0|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#37) . NIL . NATNUM . NIL . 37 .)(|∀N K.¬N=0⊃K*N=0≡K=0| . (AXIOM (TM& . |∀N K.¬N=0⊃K*N=0≡K=0|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#38) . NIL . NATNUM . NIL . 38 .)(|∀N K M.N*(K+M)=N*K+N*M| . (AXIOM (TM& . |∀N K M.N*(K+M)=N*K+N*M|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#39) . NIL . NATNUM . NIL . 39 .)(|∀N M K.(M+K)*N=M*N+K*N| . (AXIOM (TM& . |∀N M K.(M+K)*N=M*N+K*N|)) . (ADD1 PLUS TIMES M N K J I) . NIL . (NATNUM#40) . NIL . NATNUM . NIL . 40 .)(|∀INDFN ARB.(∃DEF_FUN.(∀N.DEF_FUN(0)=ARB∧DEF_FUN(N')=INDFN(N,DEF_FUN(N))))| . (AXIOM (TM& . |∀INDFN ARB.(∃DEF_FUN.(∀N.DEF_FUN(0)=ARB∧DEF_FUN(N')=INDFN(N,DEF_FUN(N))))|)) . (ADD1 M N K J I ARB2 ARB1 ARB INDFN DEF_FUN) . NIL . (INDUCTION#10) . NIL . INDUCTION . NIL . 10 .)(|¬(∃DESC.(∀N.DESC(N')<DESC(N)))| . (AXIOM (TM& . |¬(∃DESC.(∀N.DESC(N')<DESC(N)))|)) . (LESSP ADD1 M N K J I (DESC . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . INDUCTION#11 . NIL . VARIABLE .))) . NIL . (INDUCTION#11) . NIL . INDUCTION . NIL . 11 .)